$\forall$${\it es}$:ES, $p$:(E$\rightarrow$(E + Top)).
\\[0ex](causal{-}predecessor(${\it es}$;$p$) \& p{-}inject(E;E;$p$))
\\[0ex]$\Rightarrow$ ($\forall$$e$, ${\it e'}$:E. same{-}thread(${\it es}$;$p$;$e$;${\it e'}$) $\Rightarrow$ ((($e$ $<$ ${\it e'}$) $\vee$ ($e$ = ${\it e'}$)) $\vee$ (${\it e'}$ $<$ $e$)))